es:ES, P1, Q1, P2, Q2:(E), dcd_P1:(e:EDec(P1(e))), f:({e:E| P1(e)} {e:E| Q1(e)} ),
g:({e:E| P2(e)} {e:E| Q2(e)} ).
(Q1 ==f== P1 & Q2 ==g== P2)  e.(Q1(e))  (Q2(e)) ==[P1? f : g]== e.(P1(e))  (P2(e)) 

latex

Definitions	f(a), left + right, Q ==f== P, P  Q, P & Q, x:A  B(x), P  Q, E, {x:A| B(x)} , x:AB(x), x:A. B(x), Dec(P), Type, , ES, t  T, e c e', s = t, if p:P then A(p) else B fi , [P? f : g], False, A, (e < e'), S  T, suptype(S; T), {T}, b, t.1
Lemmas	conditional wf, es-E wf